<!DOCTYPE html>
<html class="writer-html5" lang="en" data-content_root="./">
<head>
  <meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />

  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>2. Basics &mdash; Mathematics in Lean v4.19.0 documentation</title>
      <link rel="stylesheet" type="text/css" href="_static/pygments.css?v=80d5e7a1" />
      <link rel="stylesheet" type="text/css" href="_static/css/theme.css?v=19f00094" />
      <link rel="stylesheet" type="text/css" href="_static/css/custom.css?v=0731ccc3" />

  
    <link rel="shortcut icon" href="_static/favicon.ico"/>
  <!--[if lt IE 9]>
    <script src="_static/js/html5shiv.min.js"></script>
  <![endif]-->
  
        <script src="_static/jquery.js?v=5d32c60e"></script>
        <script src="_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
        <script src="_static/documentation_options.js?v=7048e04d"></script>
        <script src="_static/doctools.js?v=9a2dae69"></script>
        <script src="_static/sphinx_highlight.js?v=dc90522c"></script>
        <script async="async" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="genindex.html" />
    <link rel="search" title="Search" href="search.html" />
    <link rel="next" title="3. Logic" href="C03_Logic.html" />
    <link rel="prev" title="1. Introduction" href="C01_Introduction.html" /> 
</head>

<body class="wy-body-for-nav"> 
  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side">
      <div class="wy-side-scroll">
        <div class="wy-side-nav-search" >

          
          
          <a href="index.html" class="icon icon-home">
            Mathematics in Lean
          </a>
<div role="search">
  <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
    <input type="text" name="q" placeholder="Search docs" aria-label="Search docs" />
    <input type="hidden" name="check_keywords" value="yes" />
    <input type="hidden" name="area" value="default" />
  </form>
</div>
        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul class="current">
<li class="toctree-l1"><a class="reference internal" href="C01_Introduction.html">1. Introduction</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">2. Basics</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#calculating">2.1. Calculating</a></li>
<li class="toctree-l2"><a class="reference internal" href="#proving-identities-in-algebraic-structures">2.2. Proving Identities in Algebraic Structures</a></li>
<li class="toctree-l2"><a class="reference internal" href="#using-theorems-and-lemmas">2.3. Using Theorems and Lemmas</a></li>
<li class="toctree-l2"><a class="reference internal" href="#more-examples-using-apply-and-rw">2.4. More examples using apply and rw</a></li>
<li class="toctree-l2"><a class="reference internal" href="#proving-facts-about-algebraic-structures">2.5. Proving Facts about Algebraic Structures</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C03_Logic.html">3. Logic</a></li>
<li class="toctree-l1"><a class="reference internal" href="C04_Sets_and_Functions.html">4. Sets and Functions</a></li>
<li class="toctree-l1"><a class="reference internal" href="C05_Elementary_Number_Theory.html">5. Elementary Number Theory</a></li>
<li class="toctree-l1"><a class="reference internal" href="C06_Discrete_Mathematics.html">6. Discrete Mathematics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C07_Structures.html">7. Structures</a></li>
<li class="toctree-l1"><a class="reference internal" href="C08_Hierarchies.html">8. Hierarchies</a></li>
<li class="toctree-l1"><a class="reference internal" href="C09_Groups_and_Rings.html">9. Groups and Rings</a></li>
<li class="toctree-l1"><a class="reference internal" href="C10_Linear_Algebra.html">10. Linear algebra</a></li>
<li class="toctree-l1"><a class="reference internal" href="C11_Topology.html">11. Topology</a></li>
<li class="toctree-l1"><a class="reference internal" href="C12_Differential_Calculus.html">12. Differential Calculus</a></li>
<li class="toctree-l1"><a class="reference internal" href="C13_Integration_and_Measure_Theory.html">13. Integration and Measure Theory</a></li>
</ul>
<ul>
<li class="toctree-l1"><a class="reference internal" href="genindex.html">Index</a></li>
</ul>

        </div>
      </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="index.html">Mathematics in Lean</a>
      </nav>

      <div class="wy-nav-content">
        <div class="rst-content">
          <div role="navigation" aria-label="Page navigation">
  <ul class="wy-breadcrumbs">
      <li><a href="index.html" class="icon icon-home" aria-label="Home"></a></li>
      <li class="breadcrumb-item active"><span class="section-number">2. </span>Basics</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/C02_Basics.rst.txt" rel="nofollow"> View page source</a>
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             
  <section id="basics">
<span id="id1"></span><h1><span class="section-number">2. </span>Basics<a class="headerlink" href="#basics" title="Link to this heading">&#61633;</a></h1>
<p>This chapter is designed to introduce you to the nuts and
bolts of mathematical reasoning in Lean: calculating,
applying lemmas and theorems,
and reasoning about generic structures.</p>
<section id="calculating">
<h2><span class="section-number">2.1. </span>Calculating<a class="headerlink" href="#calculating" title="Link to this heading">&#61633;</a></h2>
<p>We generally learn to carry out mathematical calculations
without thinking of them as proofs.
But when we justify each step in a calculation,
as Lean requires us to do,
the net result is a proof that the left-hand side of the calculation
is equal to the right-hand side.</p>
<p id="index-0">In Lean, stating a theorem is tantamount to stating a goal,
namely, the goal of proving the theorem.
Lean provides the rewriting tactic <code class="docutils literal notranslate"><span class="pre">rw</span></code>,
to replace the left-hand side of an identity by the right-hand side
in the goal. If <code class="docutils literal notranslate"><span class="pre">a</span></code>, <code class="docutils literal notranslate"><span class="pre">b</span></code>, and <code class="docutils literal notranslate"><span class="pre">c</span></code> are real numbers,
<code class="docutils literal notranslate"><span class="pre">mul_assoc</span> <span class="pre">a</span> <span class="pre">b</span> <span class="pre">c</span></code>  is the identity <code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">*</span> <span class="pre">b</span> <span class="pre">*</span> <span class="pre">c</span> <span class="pre">=</span> <span class="pre">a</span> <span class="pre">*</span> <span class="pre">(b</span> <span class="pre">*</span> <span class="pre">c)</span></code>
and <code class="docutils literal notranslate"><span class="pre">mul_comm</span> <span class="pre">a</span> <span class="pre">b</span></code> is the identity <code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">*</span> <span class="pre">b</span> <span class="pre">=</span> <span class="pre">b</span> <span class="pre">*</span> <span class="pre">a</span></code>.
Lean provides automation that generally eliminates the need
to refer the facts like these explicitly,
but they are useful for the purposes of illustration.
In Lean, multiplication associates to the left,
so the left-hand side of <code class="docutils literal notranslate"><span class="pre">mul_assoc</span></code> could also be written <code class="docutils literal notranslate"><span class="pre">(a</span> <span class="pre">*</span> <span class="pre">b)</span> <span class="pre">*</span> <span class="pre">c</span></code>.
However, it is generally good style to be mindful of Lean&#8217;s
notational conventions and leave out parentheses when Lean does as well.</p>
<p>Let&#8217;s try out <code class="docutils literal notranslate"><span class="pre">rw</span></code>.</p>
<div class="highlight-lean notranslate" id="index-1"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mul_comm</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="o">]</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mul_assoc</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">c</span><span class="o">]</span>
</pre></div>
</div>
<p>The <code class="docutils literal notranslate"><span class="pre">import</span></code> lines at the beginning of the associated examples file
import the theory of the real numbers from Mathlib, as well as useful automation.
For the sake of brevity,
we generally suppress information like this in the textbook.</p>
<p>You are welcome to make changes to see what happens.
You can type the <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> character as <code class="docutils literal notranslate"><span class="pre">\R</span></code> or <code class="docutils literal notranslate"><span class="pre">\real</span></code>
in VS Code.
The symbol doesn&#8217;t appear until you hit space or the tab key.
If you hover over a symbol when reading a Lean file,
VS Code will show you the syntax that can be used to enter it.
If you are curious to see all available abbreviations, you can hit Ctrl-Shift-P
and then type abbreviations to get access to the <code class="docutils literal notranslate"><span class="pre">Lean</span> <span class="pre">4:</span> <span class="pre">Show</span> <span class="pre">Unicode</span> <span class="pre">Input</span> <span class="pre">Abbreviations</span></code> command.
If your keyboard does not have an easily accessible backslash,
you can change the leading character by changing the
<code class="docutils literal notranslate"><span class="pre">lean4.input.leader</span></code> setting.</p>
<p id="index-2">When a cursor is in the middle of a tactic proof,
Lean reports on the current <em>proof state</em> in the
<em>Lean Infoview</em> window.
As you move your cursor past each step of the proof,
you can see the state change.
A typical proof state in Lean might look as follows:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="mi">1</span><span class="w"> </span><span class="n">goal</span>
<span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span>
<span class="n">h&#8321;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Prime</span><span class="w"> </span><span class="n">x</span><span class="o">,</span>
<span class="n">h&#8322;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#172;</span><span class="n">Even</span><span class="w"> </span><span class="n">x</span><span class="o">,</span>
<span class="n">h&#8323;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&gt;</span><span class="w"> </span><span class="n">x</span>
<span class="bp">&#8866;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8805;</span><span class="w"> </span><span class="mi">4</span>
</pre></div>
</div>
<p>The lines before the one that begins with <code class="docutils literal notranslate"><span class="pre">&#8866;</span></code> denote the <em>context</em>:
they are the objects and assumptions currently at play.
In this example, these include two objects, <code class="docutils literal notranslate"><span class="pre">x</span></code> and <code class="docutils literal notranslate"><span class="pre">y</span></code>,
each a natural number.
They also include three assumptions,
labelled <code class="docutils literal notranslate"><span class="pre">h&#8321;</span></code>, <code class="docutils literal notranslate"><span class="pre">h&#8322;</span></code>, and <code class="docutils literal notranslate"><span class="pre">h&#8323;</span></code>.
In Lean, everything in a context is labelled with an identifier.
You can type these subscripted labels as <code class="docutils literal notranslate"><span class="pre">h\1</span></code>, <code class="docutils literal notranslate"><span class="pre">h\2</span></code>, and <code class="docutils literal notranslate"><span class="pre">h\3</span></code>,
but any legal identifiers would do:
you can use <code class="docutils literal notranslate"><span class="pre">h1</span></code>, <code class="docutils literal notranslate"><span class="pre">h2</span></code>, <code class="docutils literal notranslate"><span class="pre">h3</span></code> instead,
or <code class="docutils literal notranslate"><span class="pre">foo</span></code>, <code class="docutils literal notranslate"><span class="pre">bar</span></code>, and <code class="docutils literal notranslate"><span class="pre">baz</span></code>.
The last line represents the <em>goal</em>,
that is, the fact to be proved.
Sometimes people use <em>target</em> for the fact to be proved,
and <em>goal</em> for the combination of the context and the target.
In practice, the intended meaning is usually clear.</p>
<p>Try proving these identities,
in each case replacing <code class="docutils literal notranslate"><span class="pre">sorry</span></code> by a tactic proof.
With the <code class="docutils literal notranslate"><span class="pre">rw</span></code> tactic, you can use a left arrow (<code class="docutils literal notranslate"><span class="pre">\l</span></code>)
to reverse an identity.
For example, <code class="docutils literal notranslate"><span class="pre">rw</span> <span class="pre">[&#8592;</span> <span class="pre">mul_assoc</span> <span class="pre">a</span> <span class="pre">b</span> <span class="pre">c]</span></code>
replaces <code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">*</span> <span class="pre">(b</span> <span class="pre">*</span> <span class="pre">c)</span></code> by <code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">*</span> <span class="pre">b</span> <span class="pre">*</span> <span class="pre">c</span></code> in the current goal. Note that
the left-pointing arrow refers to going from right to left in the identity provided
by <code class="docutils literal notranslate"><span class="pre">mul_assoc</span></code>, it has nothing to do with the left or right side of the goal.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>You can also use identities like <code class="docutils literal notranslate"><span class="pre">mul_assoc</span></code> and <code class="docutils literal notranslate"><span class="pre">mul_comm</span></code> without arguments.
In this case, the rewrite tactic tries to match the left-hand side with
an expression in the goal,
using the first pattern it finds.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mul_assoc</span><span class="o">]</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mul_comm</span><span class="o">]</span>
</pre></div>
</div>
<p>You can also provide <em>partial</em> information.
For example, <code class="docutils literal notranslate"><span class="pre">mul_comm</span> <span class="pre">a</span></code> matches any pattern of the form
<code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">*</span> <span class="pre">?</span></code> and rewrites it to <code class="docutils literal notranslate"><span class="pre">?</span> <span class="pre">*</span> <span class="pre">a</span></code>.
Try doing the first of these examples without
providing any arguments at all,
and the second with only one argument.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>You can also use <code class="docutils literal notranslate"><span class="pre">rw</span></code> with facts from the local context.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">d</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">e</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">d</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">f</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">h&#39;</span><span class="o">]</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">mul_assoc</span><span class="o">]</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">h</span><span class="o">]</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mul_assoc</span><span class="o">]</span>
</pre></div>
</div>
<p>Try these, using the theorem <code class="docutils literal notranslate"><span class="pre">sub_self</span></code> for the second one:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">f</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hyp</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">d</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hyp&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Multiple rewrite commands can be carried out with a single command,
by listing the relevant identities separated by commas inside the square brackets.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">d</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">e</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">d</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">f</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">h&#39;</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">mul_assoc</span><span class="o">,</span><span class="w"> </span><span class="n">h</span><span class="o">,</span><span class="w"> </span><span class="n">mul_assoc</span><span class="o">]</span>
</pre></div>
</div>
<p>You still see the incremental progress by placing the cursor after
a comma in any list of rewrites.</p>
<p>Another trick is that we can declare variables once and for all outside
an example or theorem. Lean then includes them automatically.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">d</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">e</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">d</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">f</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">h&#39;</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">mul_assoc</span><span class="o">,</span><span class="w"> </span><span class="n">h</span><span class="o">,</span><span class="w"> </span><span class="n">mul_assoc</span><span class="o">]</span>
</pre></div>
</div>
<p>Inspection of the tactic state at the beginning of the above proof
reveals that Lean indeed included all variables.
We can delimit the scope of the declaration by putting it
in a <code class="docutils literal notranslate"><span class="pre">section</span> <span class="pre">...</span> <span class="pre">end</span></code> block.
Finally, recall from the introduction that Lean provides us with a
command to determine the type of an expression:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="n">a</span>
<span class="k">#check</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="n">mul_comm</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">mul_comm</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="n">mul_assoc</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span>
<span class="k">#check</span><span class="w"> </span><span class="n">mul_comm</span><span class="w"> </span><span class="n">a</span>
<span class="k">#check</span><span class="w"> </span><span class="n">mul_comm</span>

<span class="kd">end</span>
</pre></div>
</div>
<p>The <code class="docutils literal notranslate"><span class="pre">#check</span></code> command works for both objects and facts.
In response to the command <code class="docutils literal notranslate"><span class="pre">#check</span> <span class="pre">a</span></code>, Lean reports that <code class="docutils literal notranslate"><span class="pre">a</span></code> has type <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code>.
In response to the command <code class="docutils literal notranslate"><span class="pre">#check</span> <span class="pre">mul_comm</span> <span class="pre">a</span> <span class="pre">b</span></code>,
Lean reports that <code class="docutils literal notranslate"><span class="pre">mul_comm</span> <span class="pre">a</span> <span class="pre">b</span></code> is a proof of the fact <code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">*</span> <span class="pre">b</span> <span class="pre">=</span> <span class="pre">b</span> <span class="pre">*</span> <span class="pre">a</span></code>.
The command <code class="docutils literal notranslate"><span class="pre">#check</span> <span class="pre">(a</span> <span class="pre">:</span> <span class="pre">&#8477;)</span></code> states our expectation that the
type of <code class="docutils literal notranslate"><span class="pre">a</span></code> is <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code>,
and Lean will raise an error if that is not the case.
We will explain the output of the last three <code class="docutils literal notranslate"><span class="pre">#check</span></code> commands later,
but in the meanwhile, you can take a look at them,
and experiment with some <code class="docutils literal notranslate"><span class="pre">#check</span></code> commands of your own.</p>
<p>Let&#8217;s try some more examples. The theorem <code class="docutils literal notranslate"><span class="pre">two_mul</span> <span class="pre">a</span></code> says
that <code class="docutils literal notranslate"><span class="pre">2</span> <span class="pre">*</span> <span class="pre">a</span> <span class="pre">=</span> <span class="pre">a</span> <span class="pre">+</span> <span class="pre">a</span></code>. The theorems <code class="docutils literal notranslate"><span class="pre">add_mul</span></code> and <code class="docutils literal notranslate"><span class="pre">mul_add</span></code>
express the distributivity of multiplication over addition,
and the theorem <code class="docutils literal notranslate"><span class="pre">add_assoc</span></code> expresses the associativity of addition.
Use the <code class="docutils literal notranslate"><span class="pre">#check</span></code> command to see the precise statements.</p>
<div class="highlight-lean notranslate" id="index-3"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mul_add</span><span class="o">,</span><span class="w"> </span><span class="n">add_mul</span><span class="o">,</span><span class="w"> </span><span class="n">add_mul</span><span class="o">]</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">add_assoc</span><span class="o">,</span><span class="w"> </span><span class="n">add_assoc</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="o">)]</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mul_comm</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">a</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">two_mul</span><span class="o">]</span>
</pre></div>
</div>
<p>Whereas it is possible to figure out what is going on in this proof
by stepping through it in the editor,
it is hard to read on its own.
Lean provides a more structured way of writing proofs like this
using the <code class="docutils literal notranslate"><span class="pre">calc</span></code> keyword.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="k">calc</span>
<span class="w">    </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">      </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mul_add</span><span class="o">,</span><span class="w"> </span><span class="n">add_mul</span><span class="o">,</span><span class="w"> </span><span class="n">add_mul</span><span class="o">]</span>
<span class="w">    </span><span class="n">_</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">      </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">add_assoc</span><span class="o">,</span><span class="w"> </span><span class="n">add_assoc</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="o">)]</span>
<span class="w">    </span><span class="n">_</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">      </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mul_comm</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">a</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">two_mul</span><span class="o">]</span>
</pre></div>
</div>
<p>Notice that the proof does <em>not</em> begin with <code class="docutils literal notranslate"><span class="pre">by</span></code>:
an expression that begins with <code class="docutils literal notranslate"><span class="pre">calc</span></code> is a <em>proof term</em>.
A <code class="docutils literal notranslate"><span class="pre">calc</span></code> expression can also be used inside a tactic proof,
but Lean interprets it as the instruction to use the resulting
proof term to solve the goal.
The <code class="docutils literal notranslate"><span class="pre">calc</span></code> syntax is finicky: the underscores and justification
have to be in the format indicated above.
Lean uses indentation to determine things like where a block
of tactics or a <code class="docutils literal notranslate"><span class="pre">calc</span></code> block begins and ends;
try changing the indentation in the proof above to see what happens.</p>
<p>One way to write a <code class="docutils literal notranslate"><span class="pre">calc</span></code> proof is to outline it first
using the <code class="docutils literal notranslate"><span class="pre">sorry</span></code> tactic for justification,
make sure Lean accepts the expression modulo these,
and then justify the individual steps using tactics.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="k">calc</span>
<span class="w">    </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">      </span><span class="gr">sorry</span>
<span class="w">    </span><span class="n">_</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">      </span><span class="gr">sorry</span>
<span class="w">    </span><span class="n">_</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">      </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Try proving the following identity using both a pure <code class="docutils literal notranslate"><span class="pre">rw</span></code> proof
and a more structured <code class="docutils literal notranslate"><span class="pre">calc</span></code> proof:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">c</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">d</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>The following exercise is a little more challenging.
You can use the theorems listed underneath.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="k">#check</span><span class="w"> </span><span class="n">pow_two</span><span class="w"> </span><span class="n">a</span>
<span class="k">#check</span><span class="w"> </span><span class="n">mul_sub</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span>
<span class="k">#check</span><span class="w"> </span><span class="n">add_mul</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span>
<span class="k">#check</span><span class="w"> </span><span class="n">add_sub</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span>
<span class="k">#check</span><span class="w"> </span><span class="n">sub_sub</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span>
<span class="k">#check</span><span class="w"> </span><span class="n">add_zero</span><span class="w"> </span><span class="n">a</span>
</pre></div>
</div>
<p id="index-4">We can also perform rewriting in an assumption in the context.
For example, <code class="docutils literal notranslate"><span class="pre">rw</span> <span class="pre">[mul_comm</span> <span class="pre">a</span> <span class="pre">b]</span> <span class="pre">at</span> <span class="pre">hyp</span></code> replaces <code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">*</span> <span class="pre">b</span></code> by <code class="docutils literal notranslate"><span class="pre">b</span> <span class="pre">*</span> <span class="pre">a</span></code>
in the assumption <code class="docutils literal notranslate"><span class="pre">hyp</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hyp</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hyp&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">d</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">hyp&#39;</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">hyp</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">mul_comm</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="n">a</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">hyp</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">two_mul</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">d</span><span class="o">)]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">hyp</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">mul_assoc</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">d</span><span class="o">]</span><span class="w"> </span><span class="n">at</span><span class="w"> </span><span class="n">hyp</span>
<span class="w">  </span><span class="n">exact</span><span class="w"> </span><span class="n">hyp</span>
</pre></div>
</div>
<p id="index-5">In the last step, the <code class="docutils literal notranslate"><span class="pre">exact</span></code> tactic can use <code class="docutils literal notranslate"><span class="pre">hyp</span></code> to solve the goal
because at that point <code class="docutils literal notranslate"><span class="pre">hyp</span></code> matches the goal exactly.</p>
<p id="index-6">We close this section by noting that Mathlib provides a
useful bit of automation with a <code class="docutils literal notranslate"><span class="pre">ring</span></code> tactic,
which is designed to prove identities in any commutative ring as long as they follow
purely from the ring axioms, without using any local assumption.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">ring</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">ring</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">ring</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">hyp</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hyp&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">d</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">hyp</span><span class="o">,</span><span class="w"> </span><span class="n">hyp&#39;</span><span class="o">]</span>
<span class="w">  </span><span class="n">ring</span>
</pre></div>
</div>
<p>The <code class="docutils literal notranslate"><span class="pre">ring</span></code> tactic is imported indirectly when we
import <code class="docutils literal notranslate"><span class="pre">Mathlib.Data.Real.Basic</span></code>,
but we will see in the next section that it can be used
for calculations on structures other than the real numbers.
It can be imported explicitly with the command
<code class="docutils literal notranslate"><span class="pre">import</span> <span class="pre">Mathlib.Tactic</span></code>.
We will see there are similar tactics for other common kind of algebraic
structures.</p>
<p>There is a variation of <code class="docutils literal notranslate"><span class="pre">rw</span></code> called <code class="docutils literal notranslate"><span class="pre">nth_rw</span></code> that allows you to replace only particular instances of an expression in the goal.
Possible matches are enumerated starting with 1,
so in the following example, <code class="docutils literal notranslate"><span class="pre">nth_rw</span> <span class="pre">2</span> <span class="pre">[h]</span></code> replaces the second
occurrence of <code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">+</span> <span class="pre">b</span></code> with <code class="docutils literal notranslate"><span class="pre">c</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">nth_rw</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">[</span><span class="n">h</span><span class="o">]</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">add_mul</span><span class="o">]</span>
</pre></div>
</div>
</section>
<section id="proving-identities-in-algebraic-structures">
<span id="id2"></span><h2><span class="section-number">2.2. </span>Proving Identities in Algebraic Structures<a class="headerlink" href="#proving-identities-in-algebraic-structures" title="Link to this heading">&#61633;</a></h2>
<p id="index-7">Mathematically, a ring consists of a collection of objects,
<span class="math notranslate nohighlight">\(R\)</span>, operations <span class="math notranslate nohighlight">\(+\)</span> <span class="math notranslate nohighlight">\(\times\)</span>, and constants <span class="math notranslate nohighlight">\(0\)</span>
and <span class="math notranslate nohighlight">\(1\)</span>, and an operation <span class="math notranslate nohighlight">\(x \mapsto -x\)</span> such that:</p>
<ul class="simple">
<li><p><span class="math notranslate nohighlight">\(R\)</span> with <span class="math notranslate nohighlight">\(+\)</span> is an <em>abelian group</em>, with <span class="math notranslate nohighlight">\(0\)</span>
as the additive identity and negation as inverse.</p></li>
<li><p>Multiplication is associative with identity <span class="math notranslate nohighlight">\(1\)</span>,
and multiplication distributes over addition.</p></li>
</ul>
<p>In Lean, the collection of objects is represented as a <em>type</em>, <code class="docutils literal notranslate"><span class="pre">R</span></code>.
The ring axioms are as follows:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">Ring</span><span class="w"> </span><span class="n">R</span><span class="o">]</span>

<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">add_assoc</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">,</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">c</span><span class="o">))</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">add_comm</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">,</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">a</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">zero_add</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">,</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">neg_add_cancel</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">,</span><span class="w"> </span><span class="bp">-</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">mul_assoc</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">,</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="o">))</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">mul_one</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">,</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">one_mul</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">mul_add</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">,</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">add_mul</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">,</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="o">)</span>
</pre></div>
</div>
<p>You will learn more about the square brackets in the first line later,
but for the time being,
suffice it to say that the declaration gives us a type, <code class="docutils literal notranslate"><span class="pre">R</span></code>,
and a ring structure on <code class="docutils literal notranslate"><span class="pre">R</span></code>.
Lean then allows us to use generic ring notation with elements of <code class="docutils literal notranslate"><span class="pre">R</span></code>,
and to make use of a library of theorems about rings.</p>
<p>The names of some of the theorems should look familiar:
they are exactly the ones we used to calculate with the real numbers
in the last section.
Lean is good not only for proving things about concrete mathematical
structures like the natural numbers and the integers,
but also for proving things about abstract structures,
characterized axiomatically, like rings.
Moreover, Lean supports <em>generic reasoning</em> about
both abstract and concrete structures,
and can be trained to recognize appropriate instances.
So any theorem about rings can be applied to concrete rings
like the integers, <code class="docutils literal notranslate"><span class="pre">&#8484;</span></code>, the rational numbers,  <code class="docutils literal notranslate"><span class="pre">&#8474;</span></code>,
and the complex numbers <code class="docutils literal notranslate"><span class="pre">&#8450;</span></code>.
It can also be applied to any instance of an abstract
structure that extends rings,
such as any ordered ring or any field.</p>
<p id="index-8">Not all important properties of the real numbers hold in an
arbitrary ring, however.
For example, multiplication on the real numbers
is commutative,
but that does not hold in general.
If you have taken a course in linear algebra,
you will recognize that, for every <span class="math notranslate nohighlight">\(n\)</span>,
the <span class="math notranslate nohighlight">\(n\)</span> by <span class="math notranslate nohighlight">\(n\)</span> matrices of real numbers
form a ring in which commutativity usually fails. If we declare <code class="docutils literal notranslate"><span class="pre">R</span></code> to be a
<em>commutative</em> ring, in fact, all the theorems
in the last section continue to hold when we replace
<code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> by <code class="docutils literal notranslate"><span class="pre">R</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">CommRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">ring</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">ring</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">ring</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">hyp</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hyp&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">d</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">hyp</span><span class="o">,</span><span class="w"> </span><span class="n">hyp&#39;</span><span class="o">]</span>
<span class="w">  </span><span class="n">ring</span>
</pre></div>
</div>
<p>We leave it to you to check that all the other proofs go through unchanged.
Notice that when a proof is short, like <code class="docutils literal notranslate"><span class="pre">by</span> <span class="pre">ring</span></code> or <code class="docutils literal notranslate"><span class="pre">by</span> <span class="pre">linarith</span></code>
or <code class="docutils literal notranslate"><span class="pre">by</span> <span class="pre">sorry</span></code>,
it is common (and permissible) to put it on the same line as
the <code class="docutils literal notranslate"><span class="pre">by</span></code>.
Good proof-writing style should strike a balance between concision and readability.</p>
<p>The goal of this section is to strengthen the skills
you have developed in the last section
and apply them to reasoning axiomatically about rings.
We will start with the axioms listed above,
and use them to derive other facts.
Most of the facts we prove are already in Mathlib.
We will give the versions we prove the same names
to help you learn the contents of the library
as well as the naming conventions.</p>
<p id="index-9">Lean provides an organizational mechanism similar
to those used in programming languages:
when a definition or theorem <code class="docutils literal notranslate"><span class="pre">foo</span></code> is introduced in a <em>namespace</em>
<code class="docutils literal notranslate"><span class="pre">bar</span></code>, its full name is <code class="docutils literal notranslate"><span class="pre">bar.foo</span></code>.
The command <code class="docutils literal notranslate"><span class="pre">open</span> <span class="pre">bar</span></code> later <em>opens</em> the namespace,
which allows us to use the shorter name <code class="docutils literal notranslate"><span class="pre">foo</span></code>.
To avoid errors due to name clashes,
in the next example we put our versions of the library
theorems in a new namespace called <code class="docutils literal notranslate"><span class="pre">MyRing.</span></code></p>
<p>The next example shows that we do not need <code class="docutils literal notranslate"><span class="pre">add_zero</span></code> or <code class="docutils literal notranslate"><span class="pre">add_neg_cancel</span></code>
as ring axioms, because they follow from the other axioms.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">namespace</span><span class="w"> </span><span class="n">MyRing</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Ring</span><span class="w"> </span><span class="n">R</span><span class="o">]</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">add_zero</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">add_comm</span><span class="o">,</span><span class="w"> </span><span class="n">zero_add</span><span class="o">]</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">add_neg_cancel</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="bp">-</span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">add_comm</span><span class="o">,</span><span class="w"> </span><span class="n">neg_add_cancel</span><span class="o">]</span>

<span class="k">#check</span><span class="w"> </span><span class="n">MyRing.add_zero</span>
<span class="k">#check</span><span class="w"> </span><span class="n">add_zero</span>

<span class="kd">end</span><span class="w"> </span><span class="n">MyRing</span>
</pre></div>
</div>
<p>The net effect is that we can temporarily reprove a theorem in the library,
and then go on using the library version after that.
But don&#8217;t cheat!
In the exercises that follow, take care to use only the
general facts about rings that we have proved earlier in this section.</p>
<p>(If you are paying careful attention, you may have noticed that we
changed the round brackets in <code class="docutils literal notranslate"><span class="pre">(R</span> <span class="pre">:</span> <span class="pre">Type*)</span></code> for
curly brackets in <code class="docutils literal notranslate"><span class="pre">{R</span> <span class="pre">:</span> <span class="pre">Type*}</span></code>.
This declares <code class="docutils literal notranslate"><span class="pre">R</span></code> to be an <em>implicit argument</em>.
We will explain what this means in a moment,
but don&#8217;t worry about it in the meanwhile.)</p>
<p>Here is a useful theorem:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">neg_add_cancel_left</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">-</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">add_assoc</span><span class="o">,</span><span class="w"> </span><span class="n">neg_add_cancel</span><span class="o">,</span><span class="w"> </span><span class="n">zero_add</span><span class="o">]</span>
</pre></div>
</div>
<p>Prove the companion version:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">add_neg_cancel_right</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="bp">-</span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Use these to prove the following:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">add_left_cancel</span><span class="w"> </span><span class="o">{</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">add_right_cancel</span><span class="w"> </span><span class="o">{</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>With enough planning, you can do each of them with three rewrites.</p>
<p id="index-10">We will now explain the use of the curly braces.
Imagine you are in a situation where you have <code class="docutils literal notranslate"><span class="pre">a</span></code>, <code class="docutils literal notranslate"><span class="pre">b</span></code>, and <code class="docutils literal notranslate"><span class="pre">c</span></code>
in your context,
as well as a hypothesis <code class="docutils literal notranslate"><span class="pre">h</span> <span class="pre">:</span> <span class="pre">a</span> <span class="pre">+</span> <span class="pre">b</span> <span class="pre">=</span> <span class="pre">a</span> <span class="pre">+</span> <span class="pre">c</span></code>,
and you would like to draw the conclusion <code class="docutils literal notranslate"><span class="pre">b</span> <span class="pre">=</span> <span class="pre">c</span></code>.
In Lean, you can apply a theorem to hypotheses and facts just
the same way that you can apply them to objects,
so you might think that <code class="docutils literal notranslate"><span class="pre">add_left_cancel</span> <span class="pre">a</span> <span class="pre">b</span> <span class="pre">c</span> <span class="pre">h</span></code> is a
proof of the fact <code class="docutils literal notranslate"><span class="pre">b</span> <span class="pre">=</span> <span class="pre">c</span></code>.
But notice that explicitly writing <code class="docutils literal notranslate"><span class="pre">a</span></code>, <code class="docutils literal notranslate"><span class="pre">b</span></code>, and <code class="docutils literal notranslate"><span class="pre">c</span></code>
is redundant, because the hypothesis <code class="docutils literal notranslate"><span class="pre">h</span></code> makes it clear that
those are the objects we have in mind.
In this case, typing a few extra characters is not onerous,
but if we wanted to apply <code class="docutils literal notranslate"><span class="pre">add_left_cancel</span></code> to more complicated expressions,
writing them would be tedious.
In cases like these,
Lean allows us to mark arguments as <em>implicit</em>,
meaning that they are supposed to be left out and inferred by other means,
such as later arguments and hypotheses.
The curly brackets in <code class="docutils literal notranslate"><span class="pre">{a</span> <span class="pre">b</span> <span class="pre">c</span> <span class="pre">:</span> <span class="pre">R}</span></code> do exactly that.
So, given the statement of the theorem above,
the correct expression is simply <code class="docutils literal notranslate"><span class="pre">add_left_cancel</span> <span class="pre">h</span></code>.</p>
<p>To illustrate, let us show that <code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">*</span> <span class="pre">0</span> <span class="pre">=</span> <span class="pre">0</span></code>
follows from the ring axioms.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">mul_zero</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="bp">&#8592;</span><span class="w"> </span><span class="n">mul_add</span><span class="o">,</span><span class="w"> </span><span class="n">add_zero</span><span class="o">,</span><span class="w"> </span><span class="n">add_zero</span><span class="o">]</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">add_left_cancel</span><span class="w"> </span><span class="n">h</span><span class="o">]</span>
</pre></div>
</div>
<p id="index-11">We have used a new trick!
If you step through the proof,
you can see what is going on.
The <code class="docutils literal notranslate"><span class="pre">have</span></code> tactic introduces a new goal,
<code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">*</span> <span class="pre">0</span> <span class="pre">+</span> <span class="pre">a</span> <span class="pre">*</span> <span class="pre">0</span> <span class="pre">=</span> <span class="pre">a</span> <span class="pre">*</span> <span class="pre">0</span> <span class="pre">+</span> <span class="pre">0</span></code>,
with the same context as the original goal.
The fact that the next line is indented indicates that Lean
is expecting a block of tactics that serves to prove this
new goal.
The indentation therefore promotes a modular style of proof:
the indented subproof establishes the goal
that was introduced by the <code class="docutils literal notranslate"><span class="pre">have</span></code>.
After that, we are back to proving the original goal,
except a new hypothesis <code class="docutils literal notranslate"><span class="pre">h</span></code> has been added:
having proved it, we are now free to use it.
At this point, the goal is exactly the result of <code class="docutils literal notranslate"><span class="pre">add_left_cancel</span> <span class="pre">h</span></code>.</p>
<p id="index-12">We could equally well have closed the proof with
<code class="docutils literal notranslate"><span class="pre">apply</span> <span class="pre">add_left_cancel</span> <span class="pre">h</span></code> or <code class="docutils literal notranslate"><span class="pre">exact</span> <span class="pre">add_left_cancel</span> <span class="pre">h</span></code>.
The <code class="docutils literal notranslate"><span class="pre">exact</span></code> tactic takes as argument a proof term which completely proves the
current goal, without creating any new goal. The <code class="docutils literal notranslate"><span class="pre">apply</span></code> tactic is a variant
whose argument is not necessarily a complete proof. The missing pieces are either
inferred automatically by Lean or become new goals to prove.
While the <code class="docutils literal notranslate"><span class="pre">exact</span></code> tactic is technically redundant since it is strictly less powerful
than <code class="docutils literal notranslate"><span class="pre">apply</span></code>, it makes proof scripts slightly clearer to
human readers and easier to maintain when the library evolves.</p>
<p>Remember that multiplication is not assumed to be commutative,
so the following theorem also requires some work.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">zero_mul</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>By now, you should also be able replace each <code class="docutils literal notranslate"><span class="pre">sorry</span></code> in the next
exercise with a proof,
still using only facts about rings that we have
established in this section.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">neg_eq_of_add_eq_zero</span><span class="w"> </span><span class="o">{</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">-</span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">eq_neg_of_add_eq_zero</span><span class="w"> </span><span class="o">{</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">-</span><span class="n">b</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">neg_zero</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="bp">-</span><span class="mi">0</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">neg_eq_of_add_eq_zero</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">add_zero</span><span class="o">]</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">neg_neg</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="bp">-</span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>We had to use the annotation <code class="docutils literal notranslate"><span class="pre">(-0</span> <span class="pre">:</span> <span class="pre">R)</span></code> instead of <code class="docutils literal notranslate"><span class="pre">0</span></code> in the third theorem
because without specifying <code class="docutils literal notranslate"><span class="pre">R</span></code>
it is impossible for Lean to infer which <code class="docutils literal notranslate"><span class="pre">0</span></code> we have in mind,
and by default it would be interpreted as a natural number.</p>
<p>In Lean, subtraction in a ring is provably equal to
addition of the additive inverse.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="bp">-</span><span class="n">b</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">sub_eq_add_neg</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span>
</pre></div>
</div>
<p>On the real numbers, it is <em>defined</em> that way:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="bp">-</span><span class="n">b</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="bp">-</span><span class="n">b</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rfl</span>
</pre></div>
</div>
<p id="index-13">The proof term <code class="docutils literal notranslate"><span class="pre">rfl</span></code> is short for &#8220;reflexivity&#8221;.
Presenting it as a proof of <code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">-</span> <span class="pre">b</span> <span class="pre">=</span> <span class="pre">a</span> <span class="pre">+</span> <span class="pre">-b</span></code> forces Lean
to unfold the definition and recognize both sides as being the same.
The <code class="docutils literal notranslate"><span class="pre">rfl</span></code> tactic does the same.
This is an instance of what is known as a <em>definitional equality</em>
in Lean&#8217;s underlying logic.
This means that not only can one rewrite with <code class="docutils literal notranslate"><span class="pre">sub_eq_add_neg</span></code>
to replace <code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">-</span> <span class="pre">b</span> <span class="pre">=</span> <span class="pre">a</span> <span class="pre">+</span> <span class="pre">-b</span></code>,
but in some contexts, when dealing with the real numbers,
you can use the two sides of the equation interchangeably.
For example, you now have enough information to prove the theorem
<code class="docutils literal notranslate"><span class="pre">self_sub</span></code> from the last section:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">self_sub</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Show that you can prove this using <code class="docutils literal notranslate"><span class="pre">rw</span></code>,
but if you replace the arbitrary ring <code class="docutils literal notranslate"><span class="pre">R</span></code> by
the real numbers, you can also prove it
using either <code class="docutils literal notranslate"><span class="pre">apply</span></code> or <code class="docutils literal notranslate"><span class="pre">exact</span></code>.</p>
<p>Lean knows that <code class="docutils literal notranslate"><span class="pre">1</span> <span class="pre">+</span> <span class="pre">1</span> <span class="pre">=</span> <span class="pre">2</span></code> holds in any ring.
With a bit of effort,
you can use that to prove the theorem <code class="docutils literal notranslate"><span class="pre">two_mul</span></code> from
the last section:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">one_add_one_eq_two</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="mi">2</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">norm_num</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">two_mul</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p id="index-14">We close this section by noting that some of the facts about
addition and negation that we established above do not
need the full strength of the ring axioms, or even
commutativity of addition. The weaker notion of a <em>group</em>
can be axiomatized as follows:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">A</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">AddGroup</span><span class="w"> </span><span class="n">A</span><span class="o">]</span>

<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">add_assoc</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">A</span><span class="o">,</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">c</span><span class="o">))</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">zero_add</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">A</span><span class="o">,</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">neg_add_cancel</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">A</span><span class="o">,</span><span class="w"> </span><span class="bp">-</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span>
</pre></div>
</div>
<p>It is conventional to use additive notation when
the group operation is commutative,
and multiplicative notation otherwise.
So Lean defines a multiplicative version as well as the
additive version (and also their abelian variants,
<code class="docutils literal notranslate"><span class="pre">AddCommGroup</span></code> and <code class="docutils literal notranslate"><span class="pre">CommGroup</span></code>).</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">G</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Group</span><span class="w"> </span><span class="n">G</span><span class="o">]</span>

<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">mul_assoc</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">,</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="o">))</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">one_mul</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">inv_mul_cancel</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">,</span><span class="w"> </span><span class="n">a</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="o">)</span>
</pre></div>
</div>
<p>If you are feeling cocky, try proving the following facts about
groups, using only these axioms.
You will need to prove a number of helper lemmas along the way.
The proofs we have carried out in this section provide some hints.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">mul_inv_cancel</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">mul_one</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">mul_inv_rev</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">G</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">b</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="bp">&#8315;&#185;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p id="index-15">Explicitly invoking those lemmas is tedious, so Mathlib provides
tactics similar to <cite>ring</cite> in order to cover most uses: <cite>group</cite>
is for non-commutative multiplicative groups, <cite>abel</cite> for abelian
additive groups, and <cite>noncomm_ring</cite> for non-commutative rings.
It may seem odd that the algebraic structures are called
<cite>Ring</cite> and <cite>CommRing</cite> while the tactics are named
<cite>noncomm_ring</cite> and <cite>ring</cite>. This is partly for historical reasons,
but also for the convenience of using a shorter name for the
tactic that deals with commutative rings, since it is used more often.</p>
</section>
<section id="using-theorems-and-lemmas">
<span id="id3"></span><h2><span class="section-number">2.3. </span>Using Theorems and Lemmas<a class="headerlink" href="#using-theorems-and-lemmas" title="Link to this heading">&#61633;</a></h2>
<p id="index-16">Rewriting is great for proving equations,
but what about other sorts of theorems?
For example, how can we prove an inequality,
like the fact that <span class="math notranslate nohighlight">\(a + e^b \le a + e^c\)</span> holds whenever <span class="math notranslate nohighlight">\(b \le c\)</span>?
We have already seen that theorems can be applied to arguments and hypotheses,
and that the <code class="docutils literal notranslate"><span class="pre">apply</span></code> and <code class="docutils literal notranslate"><span class="pre">exact</span></code> tactics can be used to solve goals.
In this section, we will make good use of these tools.</p>
<p>Consider the library theorems <code class="docutils literal notranslate"><span class="pre">le_refl</span></code> and <code class="docutils literal notranslate"><span class="pre">le_trans</span></code>:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">le_refl</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">,</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">a</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">le_trans</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">c</span><span class="o">)</span>
</pre></div>
</div>
<p>As we explain in more detail in  <a class="reference internal" href="C03_Logic.html#implication-and-the-universal-quantifier"><span class="std std-numref">Section 3.1</span></a>,
the implicit parentheses in the statement of <code class="docutils literal notranslate"><span class="pre">le_trans</span></code>
associate to the right, so it should be interpreted as <code class="docutils literal notranslate"><span class="pre">a</span> <span class="pre">&#8804;</span> <span class="pre">b</span> <span class="pre">&#8594;</span> <span class="pre">(b</span> <span class="pre">&#8804;</span> <span class="pre">c</span> <span class="pre">&#8594;</span> <span class="pre">a</span> <span class="pre">&#8804;</span> <span class="pre">c)</span></code>.
The library designers have set the arguments <code class="docutils literal notranslate"><span class="pre">a</span></code>, <code class="docutils literal notranslate"><span class="pre">b</span></code> and <code class="docutils literal notranslate"><span class="pre">c</span></code> to <code class="docutils literal notranslate"><span class="pre">le_trans</span></code> implicit,
so that Lean will <em>not</em> let you provide them explicitly (unless you
really insist, as we will discuss later).
Rather, it expects to infer them from the context in which they are used.
For example, when hypotheses <code class="docutils literal notranslate"><span class="pre">h</span> <span class="pre">:</span> <span class="pre">a</span> <span class="pre">&#8804;</span> <span class="pre">b</span></code> and  <code class="docutils literal notranslate"><span class="pre">h'</span> <span class="pre">:</span> <span class="pre">b</span> <span class="pre">&#8804;</span> <span class="pre">c</span></code>
are in the context,
all the following work:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">c</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">le_refl</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Real</span><span class="o">,</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">a</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">le_refl</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">a</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">le_trans</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">c</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">le_trans</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">c</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">le_trans</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="n">h&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">c</span><span class="o">)</span>
</pre></div>
</div>
<p id="index-17">The <code class="docutils literal notranslate"><span class="pre">apply</span></code> tactic takes a proof of a general statement or implication,
tries to match the conclusion with the current goal,
and leaves the hypotheses, if any, as new goals.
If the given proof matches the goal exactly
(modulo <em>definitional</em> equality),
you can use the <code class="docutils literal notranslate"><span class="pre">exact</span></code> tactic instead of <code class="docutils literal notranslate"><span class="pre">apply</span></code>.
So, all of these work:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8320;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8321;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">z</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">le_trans</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">apply</span><span class="w"> </span><span class="n">h&#8320;</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">apply</span><span class="w"> </span><span class="n">h&#8321;</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8320;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8321;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">z</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">le_trans</span><span class="w"> </span><span class="n">h&#8320;</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">h&#8321;</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8320;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8321;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">z</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">le_trans</span><span class="w"> </span><span class="n">h&#8320;</span><span class="w"> </span><span class="n">h&#8321;</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">le_refl</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">le_refl</span><span class="w"> </span><span class="n">x</span>
</pre></div>
</div>
<p>In the first example, applying <code class="docutils literal notranslate"><span class="pre">le_trans</span></code>
creates two goals,
and we use the dots to indicate where the proof of each begins.
The dots are optional, but they serve to <em>focus</em> the goal:
within the block introduced by the dot, only one goal is visible,
and it must be completed before the end of the block.
Here we end the first block by starting a new one with another dot.
We could just as well have decreased the indentation.
In the third example and in the last example,
we avoid going into tactic mode entirely:
<code class="docutils literal notranslate"><span class="pre">le_trans</span> <span class="pre">h&#8320;</span> <span class="pre">h&#8321;</span></code> and <code class="docutils literal notranslate"><span class="pre">le_refl</span> <span class="pre">x</span></code> are the proof terms we need.</p>
<p>Here are a few more library theorems:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">le_refl</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">a</span><span class="o">,</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">a</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">le_trans</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">c</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">lt_of_le_of_lt</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">c</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">lt_of_lt_of_le</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">c</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">lt_trans</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">c</span><span class="o">)</span>
</pre></div>
</div>
<p>Use them together with <code class="docutils literal notranslate"><span class="pre">apply</span></code> and <code class="docutils literal notranslate"><span class="pre">exact</span></code> to prove the following:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8320;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8321;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8322;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">d</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8323;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">e</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p id="index-18">In fact, Lean has a tactic that does this sort of thing automatically:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8320;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8321;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8322;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">d</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8323;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">e</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">linarith</span>
</pre></div>
</div>
<p>The <code class="docutils literal notranslate"><span class="pre">linarith</span></code> tactic is designed to handle <em>linear arithmetic</em>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#39;&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="mi">5</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">linarith</span>
</pre></div>
</div>
<p>In addition to equations and inequalities in the context,
<code class="docutils literal notranslate"><span class="pre">linarith</span></code> will use additional inequalities that you pass as arguments.
In the next example, <code class="docutils literal notranslate"><span class="pre">exp_le_exp.mpr</span> <span class="pre">h'</span></code> is a proof of
<code class="docutils literal notranslate"><span class="pre">exp</span> <span class="pre">b</span> <span class="pre">&#8804;</span> <span class="pre">exp</span> <span class="pre">c</span></code>, as we will explain in a moment.
Notice that, in Lean, we write <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">x</span></code> to denote the application
of a function <code class="docutils literal notranslate"><span class="pre">f</span></code> to the argument <code class="docutils literal notranslate"><span class="pre">x</span></code>,
exactly the same way we write <code class="docutils literal notranslate"><span class="pre">h</span> <span class="pre">x</span></code> to denote the result of
applying a fact or theorem <code class="docutils literal notranslate"><span class="pre">h</span></code> to the argument <code class="docutils literal notranslate"><span class="pre">x</span></code>.
Parentheses are only needed for compound arguments,
as in <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">(x</span> <span class="pre">+</span> <span class="pre">y)</span></code>. Without the parentheses, <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">x</span> <span class="pre">+</span> <span class="pre">y</span></code>
would be parsed as <code class="docutils literal notranslate"><span class="pre">(f</span> <span class="pre">x)</span> <span class="pre">+</span> <span class="pre">y</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">exp</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="mi">3</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">exp</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">linarith</span><span class="w"> </span><span class="o">[</span><span class="n">exp_le_exp.mpr</span><span class="w"> </span><span class="n">h&#39;</span><span class="o">]</span>
</pre></div>
</div>
<p id="index-19">Here are some more theorems in the library that can be used to establish
inequalities on the real numbers.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">exp_le_exp</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">exp</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">exp</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">exp_lt_exp</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">exp</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">exp</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">b</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">log_le_log</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">log</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">log</span><span class="w"> </span><span class="n">b</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">log_lt_log</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">log</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">log</span><span class="w"> </span><span class="n">b</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">add_le_add</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">d</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">add_le_add_left</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">c</span><span class="o">,</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">add_le_add_right</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">c</span><span class="o">,</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">c</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">add_lt_add_of_le_of_lt</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">d</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">add_lt_add_of_lt_of_le</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">d</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">add_lt_add_left</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">c</span><span class="o">,</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">add_lt_add_right</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">c</span><span class="o">,</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">c</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">add_nonneg</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">add_pos</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">add_pos_of_pos_of_nonneg</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">exp_pos</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">a</span><span class="o">,</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">exp</span><span class="w"> </span><span class="n">a</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="n">add_le_add_left</span>
</pre></div>
</div>
<p>Some of the theorems, <code class="docutils literal notranslate"><span class="pre">exp_le_exp</span></code>, <code class="docutils literal notranslate"><span class="pre">exp_lt_exp</span></code>
use a <em>bi-implication</em>, which represents the
phrase &#8220;if and only if.&#8221;
(You can type it in VS Code with <code class="docutils literal notranslate"><span class="pre">\lr</span></code> or <code class="docutils literal notranslate"><span class="pre">\iff</span></code>).
We will discuss this connective in greater detail in the next chapter.
Such a theorem can be used with <code class="docutils literal notranslate"><span class="pre">rw</span></code> to rewrite a goal to
an equivalent one:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">exp</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">exp</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">exp_le_exp</span><span class="o">]</span>
<span class="w">  </span><span class="n">exact</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>In this section, however, we will use the fact that if <code class="docutils literal notranslate"><span class="pre">h</span> <span class="pre">:</span> <span class="pre">A</span> <span class="pre">&#8596;</span> <span class="pre">B</span></code>
is such an equivalence,
then <code class="docutils literal notranslate"><span class="pre">h.mp</span></code> establishes the forward direction, <code class="docutils literal notranslate"><span class="pre">A</span> <span class="pre">&#8594;</span> <span class="pre">B</span></code>,
and <code class="docutils literal notranslate"><span class="pre">h.mpr</span></code> establishes the reverse direction, <code class="docutils literal notranslate"><span class="pre">B</span> <span class="pre">&#8594;</span> <span class="pre">A</span></code>.
Here, <code class="docutils literal notranslate"><span class="pre">mp</span></code> stands for &#8220;modus ponens&#8221; and
<code class="docutils literal notranslate"><span class="pre">mpr</span></code> stands for &#8220;modus ponens reverse.&#8221;
You can also use <code class="docutils literal notranslate"><span class="pre">h.1</span></code> and <code class="docutils literal notranslate"><span class="pre">h.2</span></code> for <code class="docutils literal notranslate"><span class="pre">h.mp</span></code> and <code class="docutils literal notranslate"><span class="pre">h.mpr</span></code>,
respectively, if you prefer.
Thus the following proof works:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8320;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8321;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">d</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">exp</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">exp</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">add_lt_add_of_lt_of_le</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">apply</span><span class="w"> </span><span class="n">add_lt_add_of_le_of_lt</span><span class="w"> </span><span class="n">h&#8320;</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">exp_lt_exp.mpr</span><span class="w"> </span><span class="n">h&#8321;</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">le_refl</span>
</pre></div>
</div>
<p>The first line, <code class="docutils literal notranslate"><span class="pre">apply</span> <span class="pre">add_lt_add_of_lt_of_le</span></code>,
creates two goals,
and once again we use a dot to separate the
proof of the first from the proof of the second.</p>
<p id="index-20">Try the following examples on your own.
The example in the middle shows you that the <code class="docutils literal notranslate"><span class="pre">norm_num</span></code>
tactic can be used to solve concrete numeric goals.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8320;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">d</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">e</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">exp</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">d</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">exp</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">e</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="gr">sorry</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="mi">0</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">norm_num</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">log</span><span class="w"> </span><span class="o">(</span><span class="mi">1</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">exp</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">log</span><span class="w"> </span><span class="o">(</span><span class="mi">1</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">exp</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">h&#8320;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">exp</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">log_le_log</span><span class="w"> </span><span class="n">h&#8320;</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>From these examples, it should be clear that being able to
find the library theorems you need constitutes an important
part of formalization.
There are a number of strategies you can use:</p>
<ul class="simple">
<li><p>You can browse Mathlib in its
<a class="reference external" href="https://github.com/leanprover-community/mathlib4">GitHub repository</a>.</p></li>
<li><p>You can use the API documentation on the Mathlib
<a class="reference external" href="https://leanprover-community.github.io/mathlib4_docs/">web pages</a>.</p></li>
<li><p>You can use <cite>Loogle &lt;https://loogle.lean-lang.org&gt;</cite>
to search Lean and Mathlib definitions and theorems by patterns.</p></li>
<li><p>You can rely on Mathlib naming conventions and Ctrl-space completion in
the editor to guess a theorem name (or Cmd-space on a Mac keyboard).
In Lean, a theorem named <code class="docutils literal notranslate"><span class="pre">A_of_B_of_C</span></code> establishes
something of the form <code class="docutils literal notranslate"><span class="pre">A</span></code> from hypotheses of the form <code class="docutils literal notranslate"><span class="pre">B</span></code> and <code class="docutils literal notranslate"><span class="pre">C</span></code>,
where <code class="docutils literal notranslate"><span class="pre">A</span></code>, <code class="docutils literal notranslate"><span class="pre">B</span></code>, and <code class="docutils literal notranslate"><span class="pre">C</span></code>
approximate the way we might read the goals out loud.
So a theorem establishing something like <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">+</span> <span class="pre">y</span> <span class="pre">&#8804;</span> <span class="pre">...</span></code> will probably
start with <code class="docutils literal notranslate"><span class="pre">add_le</span></code>.
Typing <code class="docutils literal notranslate"><span class="pre">add_le</span></code> and hitting Ctrl-space will give you some helpful choices.
Note that hitting Ctrl-space twice displays more information about the available
completions.</p></li>
<li><p>If you right-click on an existing theorem name in VS Code,
the editor will show a menu with the option to
jump to the file where the theorem is defined,
and you can find similar theorems nearby.</p></li>
<li><p>You can use the <code class="docutils literal notranslate"><span class="pre">apply?</span></code> tactic,
which tries to find the relevant theorem in the library.</p></li>
</ul>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="c1">-- apply?</span>
<span class="w">  </span><span class="n">exact</span><span class="w"> </span><span class="n">sq_nonneg</span><span class="w"> </span><span class="n">a</span>
</pre></div>
</div>
<p>To try out <code class="docutils literal notranslate"><span class="pre">apply?</span></code> in this example,
delete the <code class="docutils literal notranslate"><span class="pre">exact</span></code> command and uncomment the previous line.
Using these tricks,
see if you can find what you need to do the
next example:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">exp</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">exp</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Using the same tricks, confirm that <code class="docutils literal notranslate"><span class="pre">linarith</span></code> instead of <code class="docutils literal notranslate"><span class="pre">apply?</span></code>
can also finish the job.</p>
<p>Here is another example of an inequality:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="bp">*</span><span class="n">a</span><span class="bp">*</span><span class="n">b</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">a</span><span class="bp">^</span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="bp">^</span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">a</span><span class="bp">^</span><span class="mi">2</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="mi">2</span><span class="bp">*</span><span class="n">a</span><span class="bp">*</span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="bp">^</span><span class="mi">2</span>
<span class="w">  </span><span class="k">calc</span>
<span class="w">    </span><span class="n">a</span><span class="bp">^</span><span class="mi">2</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="mi">2</span><span class="bp">*</span><span class="n">a</span><span class="bp">*</span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="bp">^</span><span class="mi">2</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="bp">^</span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">ring</span>
<span class="w">    </span><span class="n">_</span><span class="w"> </span><span class="bp">&#8805;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">apply</span><span class="w"> </span><span class="n">pow_two_nonneg</span>

<span class="w">  </span><span class="k">calc</span>
<span class="w">    </span><span class="mi">2</span><span class="bp">*</span><span class="n">a</span><span class="bp">*</span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">2</span><span class="bp">*</span><span class="n">a</span><span class="bp">*</span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">ring</span>
<span class="w">    </span><span class="n">_</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="mi">2</span><span class="bp">*</span><span class="n">a</span><span class="bp">*</span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="bp">^</span><span class="mi">2</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="mi">2</span><span class="bp">*</span><span class="n">a</span><span class="bp">*</span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="bp">^</span><span class="mi">2</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="n">add_le_add</span><span class="w"> </span><span class="o">(</span><span class="n">le_refl</span><span class="w"> </span><span class="n">_</span><span class="o">)</span><span class="w"> </span><span class="n">h</span>
<span class="w">    </span><span class="n">_</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="bp">^</span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="bp">^</span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">ring</span>
</pre></div>
</div>
<p>Mathlib tends to put spaces around binary operations like <code class="docutils literal notranslate"><span class="pre">*</span></code> and <code class="docutils literal notranslate"><span class="pre">^</span></code>,
but in this example, the more compressed format increases readability.
There are a number of things worth noticing.
First, an expression <code class="docutils literal notranslate"><span class="pre">s</span> <span class="pre">&#8805;</span> <span class="pre">t</span></code> is definitionally equivalent to <code class="docutils literal notranslate"><span class="pre">t</span> <span class="pre">&#8804;</span> <span class="pre">s</span></code>.
In principle, this means one should be able to use them interchangeably.
But some of Lean&#8217;s automation does not recognize the equivalence,
so Mathlib tends to favor <code class="docutils literal notranslate"><span class="pre">&#8804;</span></code> over <code class="docutils literal notranslate"><span class="pre">&#8805;</span></code>.
Second, we have used the <code class="docutils literal notranslate"><span class="pre">ring</span></code> tactic extensively.
It is a real timesaver!
Finally, notice that in the second line of the
second <code class="docutils literal notranslate"><span class="pre">calc</span></code> proof,
instead of writing <code class="docutils literal notranslate"><span class="pre">by</span> <span class="pre">exact</span> <span class="pre">add_le_add</span> <span class="pre">(le_refl</span> <span class="pre">_)</span> <span class="pre">h</span></code>,
we can simply write the proof term <code class="docutils literal notranslate"><span class="pre">add_le_add</span> <span class="pre">(le_refl</span> <span class="pre">_)</span> <span class="pre">h</span></code>.</p>
<p>In fact, the only cleverness in the proof above is figuring
out the hypothesis <code class="docutils literal notranslate"><span class="pre">h</span></code>.
Once we have it, the second calculation involves only
linear arithmetic, and <code class="docutils literal notranslate"><span class="pre">linarith</span></code> can handle it:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="bp">*</span><span class="n">a</span><span class="bp">*</span><span class="n">b</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">a</span><span class="bp">^</span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="bp">^</span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">a</span><span class="bp">^</span><span class="mi">2</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="mi">2</span><span class="bp">*</span><span class="n">a</span><span class="bp">*</span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="bp">^</span><span class="mi">2</span>
<span class="w">  </span><span class="k">calc</span>
<span class="w">    </span><span class="n">a</span><span class="bp">^</span><span class="mi">2</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="mi">2</span><span class="bp">*</span><span class="n">a</span><span class="bp">*</span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="bp">^</span><span class="mi">2</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="bp">^</span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">ring</span>
<span class="w">    </span><span class="n">_</span><span class="w"> </span><span class="bp">&#8805;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">apply</span><span class="w"> </span><span class="n">pow_two_nonneg</span>
<span class="w">  </span><span class="n">linarith</span>
</pre></div>
</div>
<p>How nice! We challenge you to use these ideas to prove the
following theorem. You can use the theorem <code class="docutils literal notranslate"><span class="pre">abs_le'.mpr</span></code>.
You will also need the <code class="docutils literal notranslate"><span class="pre">constructor</span></code> tactic to split a conjunction
to two goals; see <a class="reference internal" href="C03_Logic.html#conjunction-and-biimplication"><span class="std std-numref">Section 3.4</span></a>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">|</span><span class="n">a</span><span class="bp">*</span><span class="n">b</span><span class="bp">|</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="bp">^</span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="bp">^</span><span class="mi">2</span><span class="o">)</span><span class="bp">/</span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="k">#check</span><span class="w"> </span><span class="n">abs_le&#39;.mpr</span>
</pre></div>
</div>
<p>If you managed to solve this, congratulations!
You are well on your way to becoming a master formalizer.</p>
</section>
<section id="more-examples-using-apply-and-rw">
<span id="more-on-order-and-divisibility"></span><h2><span class="section-number">2.4. </span>More examples using apply and rw<a class="headerlink" href="#more-examples-using-apply-and-rw" title="Link to this heading">&#61633;</a></h2>
<p id="index-21">The <code class="docutils literal notranslate"><span class="pre">min</span></code> function on the real numbers is uniquely characterized
by the following three facts:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">min_le_left</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">min</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">a</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">min_le_right</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">min</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">le_min</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">min</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="o">)</span>
</pre></div>
</div>
<p>Can you guess the names of the theorems that characterize
<code class="docutils literal notranslate"><span class="pre">max</span></code> in a similar way?</p>
<p>Notice that we have to apply <code class="docutils literal notranslate"><span class="pre">min</span></code> to a pair of arguments <code class="docutils literal notranslate"><span class="pre">a</span></code> and <code class="docutils literal notranslate"><span class="pre">b</span></code>
by writing <code class="docutils literal notranslate"><span class="pre">min</span> <span class="pre">a</span> <span class="pre">b</span></code> rather than <code class="docutils literal notranslate"><span class="pre">min</span> <span class="pre">(a,</span> <span class="pre">b)</span></code>.
Formally, <code class="docutils literal notranslate"><span class="pre">min</span></code> is a function of type <code class="docutils literal notranslate"><span class="pre">&#8477;</span> <span class="pre">&#8594;</span> <span class="pre">&#8477;</span> <span class="pre">&#8594;</span> <span class="pre">&#8477;</span></code>.
When we write a type like this with multiple arrows,
the convention is that the implicit parentheses associate
to the right, so the type is interpreted as <code class="docutils literal notranslate"><span class="pre">&#8477;</span> <span class="pre">&#8594;</span> <span class="pre">(&#8477;</span> <span class="pre">&#8594;</span> <span class="pre">&#8477;)</span></code>.
The net effect is that if <code class="docutils literal notranslate"><span class="pre">a</span></code> and <code class="docutils literal notranslate"><span class="pre">b</span></code> have type <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code>
then <code class="docutils literal notranslate"><span class="pre">min</span> <span class="pre">a</span></code> has type <code class="docutils literal notranslate"><span class="pre">&#8477;</span> <span class="pre">&#8594;</span> <span class="pre">&#8477;</span></code> and
<code class="docutils literal notranslate"><span class="pre">min</span> <span class="pre">a</span> <span class="pre">b</span></code> has type <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code>, so <code class="docutils literal notranslate"><span class="pre">min</span></code> acts like a function
of two arguments, as we expect. Handling multiple
arguments in this way is known as <em>currying</em>,
after the logician Haskell Curry.</p>
<p>The order of operations in Lean can also take some getting used to.
Function application binds tighter than infix operations, so the
expression <code class="docutils literal notranslate"><span class="pre">min</span> <span class="pre">a</span> <span class="pre">b</span> <span class="pre">+</span> <span class="pre">c</span></code> is interpreted as <code class="docutils literal notranslate"><span class="pre">(min</span> <span class="pre">a</span> <span class="pre">b)</span> <span class="pre">+</span> <span class="pre">c</span></code>.
With time, these conventions will become second nature.</p>
<p>Using the theorem <code class="docutils literal notranslate"><span class="pre">le_antisymm</span></code>, we can show that two
real numbers are equal if each is less than or equal to the other.
Using this and the facts above,
we can show that <code class="docutils literal notranslate"><span class="pre">min</span></code> is commutative:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">min</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">min</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">le_antisymm</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="k">show</span><span class="w"> </span><span class="n">min</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">min</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">a</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">le_min</span>
<span class="w">    </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">apply</span><span class="w"> </span><span class="n">min_le_right</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">min_le_left</span>
<span class="w">  </span><span class="bp">&#183;</span><span class="w"> </span><span class="k">show</span><span class="w"> </span><span class="n">min</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">min</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">le_min</span>
<span class="w">    </span><span class="bp">&#183;</span><span class="w"> </span><span class="n">apply</span><span class="w"> </span><span class="n">min_le_right</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">min_le_left</span>
</pre></div>
</div>
<p id="index-22">Here we have used dots to separate proofs of
different goals.
Our usage is inconsistent:
at the outer level,
we use dots and indentation for both goals,
whereas for the nested proofs,
we use dots only until a single goal remains.
Both conventions are reasonable and useful.
We also use the <code class="docutils literal notranslate"><span class="pre">show</span></code> tactic to structure
the proof
and indicate what is being proved in each block.
The proof still works without the <code class="docutils literal notranslate"><span class="pre">show</span></code> commands,
but using them makes the proof easier to read and maintain.</p>
<p>It may bother you that the proof is repetitive.
To foreshadow skills you will learn later on,
we note that one way to avoid the repetition
is to state a local lemma and then use it:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">min</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">min</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">,</span><span class="w"> </span><span class="n">min</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">min</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">    </span><span class="n">intro</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">le_min</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">min_le_right</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">min_le_left</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">le_antisymm</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">h</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>We will say more about the universal quantifier in
<a class="reference internal" href="C03_Logic.html#implication-and-the-universal-quantifier"><span class="std std-numref">Section 3.1</span></a>,
but suffice it to say here that the hypothesis
<code class="docutils literal notranslate"><span class="pre">h</span></code> says that the desired inequality holds for
any <code class="docutils literal notranslate"><span class="pre">x</span></code> and <code class="docutils literal notranslate"><span class="pre">y</span></code>,
and the <code class="docutils literal notranslate"><span class="pre">intro</span></code> tactic introduces an arbitrary
<code class="docutils literal notranslate"><span class="pre">x</span></code> and <code class="docutils literal notranslate"><span class="pre">y</span></code> to establish the conclusion.
The first <code class="docutils literal notranslate"><span class="pre">apply</span></code> after <code class="docutils literal notranslate"><span class="pre">le_antisymm</span></code> implicitly
uses <code class="docutils literal notranslate"><span class="pre">h</span> <span class="pre">a</span> <span class="pre">b</span></code>, whereas the second one uses <code class="docutils literal notranslate"><span class="pre">h</span> <span class="pre">b</span> <span class="pre">a</span></code>.</p>
<p id="index-23">Another solution is to use the <code class="docutils literal notranslate"><span class="pre">repeat</span></code> tactic,
which applies a tactic (or a block) as many times
as it can.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">min</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">min</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">le_antisymm</span>
<span class="w">  </span><span class="n">repeat</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">le_min</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">min_le_right</span>
<span class="w">    </span><span class="n">apply</span><span class="w"> </span><span class="n">min_le_left</span>
</pre></div>
</div>
<p>We encourage you to prove the following as exercises.
You can use either of the tricks just described to shorten the first.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">max</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">max</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">min</span><span class="w"> </span><span class="o">(</span><span class="n">min</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">min</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">(</span><span class="n">min</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Of course, you are welcome to prove the associativity of <code class="docutils literal notranslate"><span class="pre">max</span></code> as well.</p>
<p>It is an interesting fact that <code class="docutils literal notranslate"><span class="pre">min</span></code> distributes over <code class="docutils literal notranslate"><span class="pre">max</span></code>
the way that multiplication distributes over addition,
and vice-versa.
In other words, on the real numbers, we have the identity
<code class="docutils literal notranslate"><span class="pre">min</span> <span class="pre">a</span> <span class="pre">(max</span> <span class="pre">b</span> <span class="pre">c)</span> <span class="pre">=</span> <span class="pre">max</span> <span class="pre">(min</span> <span class="pre">a</span> <span class="pre">b)</span> <span class="pre">(min</span> <span class="pre">a</span> <span class="pre">c)</span></code>
as well as the corresponding version with <code class="docutils literal notranslate"><span class="pre">max</span></code> and <code class="docutils literal notranslate"><span class="pre">min</span></code>
switched.
But in the next section we will see that this does <em>not</em> follow
from the transitivity and reflexivity of <code class="docutils literal notranslate"><span class="pre">&#8804;</span></code> and
the characterizing properties of <code class="docutils literal notranslate"><span class="pre">min</span></code> and <code class="docutils literal notranslate"><span class="pre">max</span></code> enumerated above.
We need to use the fact that <code class="docutils literal notranslate"><span class="pre">&#8804;</span></code> on the real numbers is a <em>total order</em>,
which is to say,
it satisfies <code class="docutils literal notranslate"><span class="pre">&#8704;</span> <span class="pre">x</span> <span class="pre">y,</span> <span class="pre">x</span> <span class="pre">&#8804;</span> <span class="pre">y</span> <span class="pre">&#8744;</span> <span class="pre">y</span> <span class="pre">&#8804;</span> <span class="pre">x</span></code>.
Here the disjunction symbol, <code class="docutils literal notranslate"><span class="pre">&#8744;</span></code>, represents &#8220;or&#8221;.
In the first case, we have <code class="docutils literal notranslate"><span class="pre">min</span> <span class="pre">x</span> <span class="pre">y</span> <span class="pre">=</span> <span class="pre">x</span></code>,
and in the second case, we have <code class="docutils literal notranslate"><span class="pre">min</span> <span class="pre">x</span> <span class="pre">y</span> <span class="pre">=</span> <span class="pre">y</span></code>.
We will learn how to reason by cases in <a class="reference internal" href="C03_Logic.html#disjunction"><span class="std std-numref">Section 3.5</span></a>,
but for now we will stick to examples that don&#8217;t require the case split.</p>
<p>Here is one such example:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">aux</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">min</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">min</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">min</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">min</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>It is clear that <code class="docutils literal notranslate"><span class="pre">aux</span></code> provides one of the two inequalities
needed to prove the equality,
but applying it to suitable values yields the other direction
as well.
As a hint, you can use the theorem <code class="docutils literal notranslate"><span class="pre">add_neg_cancel_right</span></code>
and the <code class="docutils literal notranslate"><span class="pre">linarith</span></code> tactic.</p>
<p id="index-24">Lean&#8217;s naming convention is made manifest
in the library&#8217;s name for the triangle inequality:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">abs_add</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">,</span><span class="w"> </span><span class="bp">|</span><span class="n">a</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="bp">|</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="bp">|</span><span class="n">a</span><span class="bp">|</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="bp">|</span><span class="n">b</span><span class="bp">|</span><span class="o">)</span>
</pre></div>
</div>
<p>Use it to prove the following variant, using also <code class="docutils literal notranslate"><span class="pre">add_sub_cancel_right</span></code>:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">|</span><span class="n">a</span><span class="bp">|</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="bp">|</span><span class="n">b</span><span class="bp">|</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="bp">|</span><span class="n">a</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">b</span><span class="bp">|</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">end</span>
</pre></div>
</div>
<p>See if you can do this in three lines or less.
You can use the theorem <code class="docutils literal notranslate"><span class="pre">sub_add_cancel</span></code>.</p>
<p id="index-25">Another important relation that we will make use of
in the sections to come is the divisibility relation
on the natural numbers, <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">&#8739;</span> <span class="pre">y</span></code>.
Be careful: the divisibility symbol is <em>not</em> the
ordinary bar on your keyboard.
Rather, it is a unicode character obtained by
typing <code class="docutils literal notranslate"><span class="pre">\|</span></code> in VS Code.
By convention, Mathlib uses <code class="docutils literal notranslate"><span class="pre">dvd</span></code>
to refer to it in theorem names.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8320;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#8321;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">z</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">dvd_trans</span><span class="w"> </span><span class="n">h&#8320;</span><span class="w"> </span><span class="n">h&#8321;</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">dvd_mul_of_dvd_left</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">dvd_mul_left</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">apply</span><span class="w"> </span><span class="n">dvd_mul_left</span>
</pre></div>
</div>
<p>In the last example, the exponent is a natural
number, and applying <code class="docutils literal notranslate"><span class="pre">dvd_mul_left</span></code>
forces Lean to expand the definition of <code class="docutils literal notranslate"><span class="pre">x^2</span></code> to
<code class="docutils literal notranslate"><span class="pre">x^1</span> <span class="pre">*</span> <span class="pre">x</span></code>.
See if you can guess the names of the theorems
you need to prove the following:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">w</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8739;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">z</span><span class="o">)</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">w</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="kd">end</span>
</pre></div>
</div>
<p id="index-26">With respect to divisibility, the <em>greatest common divisor</em>,
<code class="docutils literal notranslate"><span class="pre">gcd</span></code>, and least common multiple, <code class="docutils literal notranslate"><span class="pre">lcm</span></code>,
are analogous to <code class="docutils literal notranslate"><span class="pre">min</span></code> and <code class="docutils literal notranslate"><span class="pre">max</span></code>.
Since every number divides <code class="docutils literal notranslate"><span class="pre">0</span></code>,
<code class="docutils literal notranslate"><span class="pre">0</span></code> is really the greatest element with respect to divisibility:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">Nat.gcd_zero_right</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.gcd</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">n</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">Nat.gcd_zero_left</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.gcd</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">n</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">Nat.lcm_zero_right</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.lcm</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">Nat.lcm_zero_left</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.lcm</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span>
</pre></div>
</div>
<p>See if you can guess the names of the theorems you will need to
prove the following:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat.gcd</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">Nat.gcd</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>Hint: you can use <code class="docutils literal notranslate"><span class="pre">dvd_antisymm</span></code>, but if you do, Lean will
complain that the expression is ambiguous between the generic
theorem and the version <code class="docutils literal notranslate"><span class="pre">Nat.dvd_antisymm</span></code>,
the one specifically for the natural numbers.
You can use <code class="docutils literal notranslate"><span class="pre">_root_.dvd_antisymm</span></code> to specify the generic one;
either one will work.</p>
</section>
<section id="proving-facts-about-algebraic-structures">
<span id="id4"></span><h2><span class="section-number">2.5. </span>Proving Facts about Algebraic Structures<a class="headerlink" href="#proving-facts-about-algebraic-structures" title="Link to this heading">&#61633;</a></h2>
<p id="index-27">In <a class="reference internal" href="#proving-identities-in-algebraic-structures"><span class="std std-numref">Section 2.2</span></a>,
we saw that many common identities governing the real numbers hold
in more general classes of algebraic structures,
such as commutative rings.
We can use any axioms we want to describe an algebraic structure,
not just equations.
For example, a <em>partial order</em> consists of a set with a
binary relation that is reflexive, transitive, and antisymmetric.
like <code class="docutils literal notranslate"><span class="pre">&#8804;</span></code> on the real numbers.
Lean knows about partial orders:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">PartialOrder</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">y</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">le_refl</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">x</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">le_trans</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">z</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">le_antisymm</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">y</span><span class="o">)</span>
</pre></div>
</div>
<p>Here we are adopting the Mathlib convention of using
letters like <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>, <code class="docutils literal notranslate"><span class="pre">&#946;</span></code>, and <code class="docutils literal notranslate"><span class="pre">&#947;</span></code>
(entered as <code class="docutils literal notranslate"><span class="pre">\a</span></code>, <code class="docutils literal notranslate"><span class="pre">\b</span></code>, and <code class="docutils literal notranslate"><span class="pre">\g</span></code>)
for arbitrary types.
The library often uses letters like <code class="docutils literal notranslate"><span class="pre">R</span></code> and <code class="docutils literal notranslate"><span class="pre">G</span></code>
for the carriers of algebraic structures like rings and groups,
respectively,
but in general Greek letters are used for types,
especially when there is little or no structure
associated with them.</p>
<p>Associated to any partial order, <code class="docutils literal notranslate"><span class="pre">&#8804;</span></code>,
there is also a <em>strict partial order</em>, <code class="docutils literal notranslate"><span class="pre">&lt;</span></code>,
which acts somewhat like <code class="docutils literal notranslate"><span class="pre">&lt;</span></code> on the real numbers.
Saying that <code class="docutils literal notranslate"><span class="pre">x</span></code> is less than <code class="docutils literal notranslate"><span class="pre">y</span></code> in this order
is equivalent to saying that it is less-than-or-equal to <code class="docutils literal notranslate"><span class="pre">y</span></code>
and not equal to <code class="docutils literal notranslate"><span class="pre">y</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">y</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">lt_irrefl</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#172;</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">x</span><span class="o">))</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">lt_trans</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">z</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">lt_of_le_of_lt</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">z</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">lt_of_lt_of_le</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">z</span><span class="o">)</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">lt_iff_le_and_ne</span>
</pre></div>
</div>
<p>In this example, the symbol <code class="docutils literal notranslate"><span class="pre">&#8743;</span></code> stands for &#8220;and,&#8221;
the symbol <code class="docutils literal notranslate"><span class="pre">&#172;</span></code> stands for &#8220;not,&#8221; and
<code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">&#8800;</span> <span class="pre">y</span></code> abbreviates <code class="docutils literal notranslate"><span class="pre">&#172;</span> <span class="pre">(x</span> <span class="pre">=</span> <span class="pre">y)</span></code>.
In <a class="reference internal" href="C03_Logic.html#logic"><span class="std std-numref">Chapter 3</span></a>, you will learn how to use
these logical connectives to <em>prove</em> that <code class="docutils literal notranslate"><span class="pre">&lt;</span></code>
has the properties indicated.</p>
<p id="index-28">A <em>lattice</em> is a structure that extends a partial
order with operations <code class="docutils literal notranslate"><span class="pre">&#8851;</span></code> and <code class="docutils literal notranslate"><span class="pre">&#8852;</span></code> that are
analogous to <code class="docutils literal notranslate"><span class="pre">min</span></code> and <code class="docutils literal notranslate"><span class="pre">max</span></code> on the real numbers:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Lattice</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">y</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">inf_le_left</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">x</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">inf_le_right</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">y</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">le_inf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">y</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">y</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">le_sup_left</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">y</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">le_sup_right</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">y</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">sup_le</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">z</span><span class="o">)</span>
</pre></div>
</div>
<p>The characterizations of <code class="docutils literal notranslate"><span class="pre">&#8851;</span></code> and <code class="docutils literal notranslate"><span class="pre">&#8852;</span></code> justify calling them
the <em>greatest lower bound</em> and <em>least upper bound</em>, respectively.
You can type them in VS code using <code class="docutils literal notranslate"><span class="pre">\glb</span></code> and <code class="docutils literal notranslate"><span class="pre">\lub</span></code>.
The symbols are also often called then <em>infimum</em> and
the <em>supremum</em>,
and Mathlib refers to them as <code class="docutils literal notranslate"><span class="pre">inf</span></code> and <code class="docutils literal notranslate"><span class="pre">sup</span></code> in
theorem names.
To further complicate matters,
they are also often called <em>meet</em> and <em>join</em>.
Therefore, if you work with lattices,
you have to keep the following dictionary in mind:</p>
<ul class="simple">
<li><p><code class="docutils literal notranslate"><span class="pre">&#8851;</span></code> is the <em>greatest lower bound</em>, <em>infimum</em>, or <em>meet</em>.</p></li>
<li><p><code class="docutils literal notranslate"><span class="pre">&#8852;</span></code> is the <em>least upper bound</em>, <em>supremum</em>, or <em>join</em>.</p></li>
</ul>
<p>Some instances of lattices include:</p>
<ul class="simple">
<li><p><code class="docutils literal notranslate"><span class="pre">min</span></code> and <code class="docutils literal notranslate"><span class="pre">max</span></code> on any total order, such as the integers or real numbers with <code class="docutils literal notranslate"><span class="pre">&#8804;</span></code></p></li>
<li><p><code class="docutils literal notranslate"><span class="pre">&#8745;</span></code> and <code class="docutils literal notranslate"><span class="pre">&#8746;</span></code> on the collection of subsets of some domain, with the ordering <code class="docutils literal notranslate"><span class="pre">&#8838;</span></code></p></li>
<li><p><code class="docutils literal notranslate"><span class="pre">&#8743;</span></code> and <code class="docutils literal notranslate"><span class="pre">&#8744;</span></code> on boolean truth values, with ordering <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">&#8804;</span> <span class="pre">y</span></code> if either <code class="docutils literal notranslate"><span class="pre">x</span></code> is false or <code class="docutils literal notranslate"><span class="pre">y</span></code> is true</p></li>
<li><p><code class="docutils literal notranslate"><span class="pre">gcd</span></code> and <code class="docutils literal notranslate"><span class="pre">lcm</span></code> on the natural numbers (or positive natural numbers), with the divisibility ordering, <code class="docutils literal notranslate"><span class="pre">&#8739;</span></code></p></li>
<li><p>the collection of linear subspaces of a vector space,
where the greatest lower bound is given by the intersection,
the least upper bound is given by the sum of the two spaces,
and the ordering is inclusion</p></li>
<li><p>the collection of topologies on a set (or, in Lean, a type),
where the greatest lower bound of two topologies consists of
the topology that is generated by their union,
the least upper bound is their intersection,
and the ordering is reverse inclusion</p></li>
</ul>
<p>You can check that, as with <code class="docutils literal notranslate"><span class="pre">min</span></code> / <code class="docutils literal notranslate"><span class="pre">max</span></code> and <code class="docutils literal notranslate"><span class="pre">gcd</span></code> / <code class="docutils literal notranslate"><span class="pre">lcm</span></code>,
you can prove the commutativity and associativity of the infimum and supremum
using only their characterizing axioms,
together with <code class="docutils literal notranslate"><span class="pre">le_refl</span></code> and <code class="docutils literal notranslate"><span class="pre">le_trans</span></code>.</p>
<p id="index-29">Using <code class="docutils literal notranslate"><span class="pre">apply</span> <span class="pre">le_trans</span></code> when seeing a goal <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">&#8804;</span> <span class="pre">z</span></code> is not a great idea.
Indeed Lean has no way to guess which intermediate element <code class="docutils literal notranslate"><span class="pre">y</span></code> we
want to use.
So <code class="docutils literal notranslate"><span class="pre">apply</span> <span class="pre">le_trans</span></code> produces three goals that look like <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">&#8804;</span> <span class="pre">?a</span></code>, <code class="docutils literal notranslate"><span class="pre">?a</span> <span class="pre">&#8804;</span> <span class="pre">z</span></code>
and <code class="docutils literal notranslate"><span class="pre">&#945;</span></code> where <code class="docutils literal notranslate"><span class="pre">?a</span></code> (probably with a more complicated auto-generated name) stands
for the mysterious <code class="docutils literal notranslate"><span class="pre">y</span></code>.
The last goal, with type <code class="docutils literal notranslate"><span class="pre">&#945;</span></code>, is to provide the value of <code class="docutils literal notranslate"><span class="pre">y</span></code>.
It comes lasts because Lean hopes to automatically infer it from the proof of
the first goal <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">&#8804;</span> <span class="pre">?a</span></code>.
In order to avoid this unappealing situation, you can use the <code class="docutils literal notranslate"><span class="pre">calc</span></code> tactic
to explicitly provide <code class="docutils literal notranslate"><span class="pre">y</span></code>.
Alternatively, you can use the <code class="docutils literal notranslate"><span class="pre">trans</span></code> tactic
which takes <code class="docutils literal notranslate"><span class="pre">y</span></code> as an argument and produces the expected goals <code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">&#8804;</span> <span class="pre">y</span></code> and
<code class="docutils literal notranslate"><span class="pre">y</span> <span class="pre">&#8804;</span> <span class="pre">z</span></code>.
Of course you can also avoid this issue by providing directly a full proof such as
<code class="docutils literal notranslate"><span class="pre">exact</span> <span class="pre">le_trans</span> <span class="pre">inf_le_left</span> <span class="pre">inf_le_right</span></code>, but this requires a lot more
planning.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="o">(</span><span class="n">y</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">z</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="o">(</span><span class="n">y</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">z</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>You can find these theorems in the Mathlib as <code class="docutils literal notranslate"><span class="pre">inf_comm</span></code>, <code class="docutils literal notranslate"><span class="pre">inf_assoc</span></code>,
<code class="docutils literal notranslate"><span class="pre">sup_comm</span></code>, and <code class="docutils literal notranslate"><span class="pre">sup_assoc</span></code>, respectively.</p>
<p>Another good exercise is to prove the <em>absorption laws</em>
using only those axioms:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">absorb1</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">absorb2</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>These can be found in Mathlib with the names <code class="docutils literal notranslate"><span class="pre">inf_sup_self</span></code> and <code class="docutils literal notranslate"><span class="pre">sup_inf_self</span></code>.</p>
<p>A lattice that satisfies the additional identities
<code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">&#8851;</span> <span class="pre">(y</span> <span class="pre">&#8852;</span> <span class="pre">z)</span> <span class="pre">=</span> <span class="pre">(x</span> <span class="pre">&#8851;</span> <span class="pre">y)</span> <span class="pre">&#8852;</span> <span class="pre">(x</span> <span class="pre">&#8851;</span> <span class="pre">z)</span></code> and
<code class="docutils literal notranslate"><span class="pre">x</span> <span class="pre">&#8852;</span> <span class="pre">(y</span> <span class="pre">&#8851;</span> <span class="pre">z)</span> <span class="pre">=</span> <span class="pre">(x</span> <span class="pre">&#8852;</span> <span class="pre">y)</span> <span class="pre">&#8851;</span> <span class="pre">(x</span> <span class="pre">&#8852;</span> <span class="pre">z)</span></code>
is called a <em>distributive lattice</em>. Lean knows about these too:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">DistribLattice</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">inf_sup_left</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="o">(</span><span class="n">y</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">z</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">z</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">inf_sup_right</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">z</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">sup_inf_left</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">z</span><span class="o">))</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">sup_inf_right</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">z</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="o">(</span><span class="n">y</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">z</span><span class="o">))</span>
</pre></div>
</div>
<p>The left and right versions are easily shown to be
equivalent, given the commutativity of <code class="docutils literal notranslate"><span class="pre">&#8851;</span></code> and <code class="docutils literal notranslate"><span class="pre">&#8852;</span></code>.
It is a good exercise to show that not every lattice
is distributive
by providing an explicit description of a
nondistributive lattice with finitely many elements.
It is also a good exercise to show that in any lattice,
either distributivity law implies the other:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Lattice</span><span class="w"> </span><span class="n">&#945;</span><span class="o">]</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">,</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="o">(</span><span class="n">y</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">z</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">z</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="o">,</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">z</span><span class="o">))</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8852;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8851;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>It is possible to combine axiomatic structures into larger ones.
For example, a <em>strict ordered ring</em> consists of a ring together
with a partial order on the carrier
satisfying additional axioms that say that the ring operations
are compatible with the order:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">R</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">Ring</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">PartialOrder</span><span class="w"> </span><span class="n">R</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">IsStrictOrderedRing</span><span class="w"> </span><span class="n">R</span><span class="o">]</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">R</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">add_le_add_left</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">c</span><span class="o">,</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">b</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">mul_pos</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="o">)</span>
</pre></div>
</div>
<p><a class="reference internal" href="C03_Logic.html#logic"><span class="std std-numref">Chapter 3</span></a> will provide the means to derive the following from <code class="docutils literal notranslate"><span class="pre">mul_pos</span></code>
and the definition of <code class="docutils literal notranslate"><span class="pre">&lt;</span></code>:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">mul_nonneg</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">b</span><span class="o">)</span>
</pre></div>
</div>
<p>It is then an extended exercise to show that many common facts
used to reason about arithmetic and the ordering on the real
numbers hold generically for any ordered ring.
Here are a couple of examples you can try,
using only properties of rings, partial orders, and the facts
enumerated in the last two examples (beware that those rings are
not assumed to be commutative, so the <cite>ring</cite> tactic is not available):</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">h&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">c</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p id="index-30">Finally, here is one last example.
A <em>metric space</em> consists of a set equipped with a notion of
distance, <code class="docutils literal notranslate"><span class="pre">dist</span> <span class="pre">x</span> <span class="pre">y</span></code>,
mapping any pair of elements to a real number.
The distance function is assumed to satisfy the following axioms:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">X</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">MetricSpace</span><span class="w"> </span><span class="n">X</span><span class="o">]</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">X</span><span class="o">)</span>

<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">dist_self</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">dist</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">dist_comm</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">dist</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">dist</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">x</span><span class="o">)</span>
<span class="k">#check</span><span class="w"> </span><span class="o">(</span><span class="n">dist_triangle</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">dist</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">dist</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">dist</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="o">)</span>
</pre></div>
</div>
<p>Having mastered this section,
you can show that it follows from these axioms that distances are
always nonnegative:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">X</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">dist</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
<p>We recommend making use of the theorem <code class="docutils literal notranslate"><span class="pre">nonneg_of_mul_nonneg_left</span></code>.
As you may have guessed, this theorem is called <code class="docutils literal notranslate"><span class="pre">dist_nonneg</span></code> in Mathlib.</p>
</section>
</section>


           </div>
          </div>
          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
        <a href="C01_Introduction.html" class="btn btn-neutral float-left" title="1. Introduction" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
        <a href="C03_Logic.html" class="btn btn-neutral float-right" title="3. Logic" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
    </div>

  <hr/>

  <div role="contentinfo">
    <p>&#169; Copyright 2020-2025, Jeremy Avigad, Patrick Massot. Text licensed under CC BY 4.0.</p>
  </div>

  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
    provided by <a href="https://readthedocs.org">Read the Docs</a>.
   

</footer>
        </div>
      </div>
    </section>
  </div>
  <script>
      jQuery(function () {
          SphinxRtdTheme.Navigation.enable(true);
      });
  </script> 

</body>
</html>